Search results for "Proof theory"

showing 3 items of 3 documents

The Syllogistic with Unity

2011

We extend the language of the classical syllogisms with the sentence-forms “At most 1 p is a q” and “More than 1 p is a q”. We show that the resulting logic does not admit a finite set of syllogism-like rules whose associated derivation relation is sound and complete, even when reductio ad absurdum is allowed.

logic and natural languageFOS: Computer and information sciencesPure mathematicsComputer Science - Logic in Computer Sciencecomputational complexityComputational complexity theoryComputational logicSyllogismMathematics - Logicproof theorysyllogismsDerivation relationLogic in Computer Science (cs.LO)Reductio ad absurdumPhilosophyPhilosophy of logicProof theoryCalculusFOS: MathematicsF.4.0Logic (math.LO)Finite setMathematics03B65
researchProduct

Inductive types in homotopy type theory

2012

Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof s…

FOS: Computer and information sciencesComputer Science - Logic in Computer Science03B15 03B70 03F500102 computer and information sciences01 natural sciencesComputer Science::Logic in Computer ScienceFOS: MathematicsA¹ homotopy theoryCategory Theory (math.CT)0101 mathematicsMathematicsHomotopy lifting propertyType theory inductive types homotopy-initial algebraHomotopy010102 general mathematicsMathematics - Category TheoryIntuitionistic type theoryMathematics - LogicSettore MAT/01 - Logica MatematicaLogic in Computer Science (cs.LO)Algebran-connectedType theoryTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES010201 computation theory & mathematicsProof theoryTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSHomotopy type theoryComputer Science::Programming LanguagesLogic (math.LO)
researchProduct

The monadic quantifier alternation hierarchy over grids and pictures

1998

The subject of this paper is the expressive power of monadic second-order logic over two-dimensional grids. We give a new, self-contained game-theoretical proof of the nonexpressibility results of Matz and Thomas. As we show, this implies the strictness of the monadic second-order quantifier alternation hierarchy over grids.

Discrete mathematicsTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESFinite-state machineComputational complexity theoryHierarchy (mathematics)Proof theoryComputer Science::Logic in Computer ScienceQuantifier (linguistics)Subject (grammar)Alternation (formal language theory)Monadic predicate calculusMathematics
researchProduct